Left Termination of the query pattern prime_in_1(g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).
prime(s(s(X))) :- pr(s(s(X)), s(X)).
pr(X, s(0)).
pr(X, s(s(Y))) :- ','(not_divides(s(s(Y)), X), pr(X, s(Y))).
not_divides(Y, X) :- ','(div(X, Y, U), ','(times(U, Y, Z), neq(X, Z))).
neq(s(X), 0).
neq(0, s(X)).
neq(s(X), s(Y)) :- neq(X, Y).
times(0, Y, 0).
times(s(X), Y, Z) :- ','(times(X, Y, U), add(U, Y, Z)).
add(X, 0, X).
add(0, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).

Queries:

prime(g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PRIME_IN(s(s(X))) → U41(X, pr_in(s(s(X)), s(X)))
PRIME_IN(s(s(X))) → PR_IN(s(s(X)), s(X))
PR_IN(X, s(s(Y))) → U51(X, Y, not_divides_in(s(s(Y)), X))
PR_IN(X, s(s(Y))) → NOT_DIVIDES_IN(s(s(Y)), X)
NOT_DIVIDES_IN(Y, X) → U71(Y, X, div_in(X, Y, U))
NOT_DIVIDES_IN(Y, X) → DIV_IN(X, Y, U)
DIV_IN(X, Y, Z) → U11(X, Y, Z, quot_in(X, Y, Y, Z))
DIV_IN(X, Y, Z) → QUOT_IN(X, Y, Y, Z)
QUOT_IN(X, 0, s(Z), s(U)) → U31(X, Z, U, quot_in(X, s(Z), s(Z), U))
QUOT_IN(X, 0, s(Z), s(U)) → QUOT_IN(X, s(Z), s(Z), U)
QUOT_IN(s(X), s(Y), Z, U) → U21(X, Y, Z, U, quot_in(X, Y, Z, U))
QUOT_IN(s(X), s(Y), Z, U) → QUOT_IN(X, Y, Z, U)
U71(Y, X, div_out(X, Y, U)) → U81(Y, X, times_in(U, Y, Z))
U71(Y, X, div_out(X, Y, U)) → TIMES_IN(U, Y, Z)
TIMES_IN(s(X), Y, Z) → U111(X, Y, Z, times_in(X, Y, U))
TIMES_IN(s(X), Y, Z) → TIMES_IN(X, Y, U)
U111(X, Y, Z, times_out(X, Y, U)) → U121(X, Y, Z, add_in(U, Y, Z))
U111(X, Y, Z, times_out(X, Y, U)) → ADD_IN(U, Y, Z)
ADD_IN(s(X), Y, s(Z)) → U131(X, Y, Z, add_in(X, Y, Z))
ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)
U81(Y, X, times_out(U, Y, Z)) → U91(Y, X, neq_in(X, Z))
U81(Y, X, times_out(U, Y, Z)) → NEQ_IN(X, Z)
NEQ_IN(s(X), s(Y)) → U101(X, Y, neq_in(X, Y))
NEQ_IN(s(X), s(Y)) → NEQ_IN(X, Y)
U51(X, Y, not_divides_out(s(s(Y)), X)) → U61(X, Y, pr_in(X, s(Y)))
U51(X, Y, not_divides_out(s(s(Y)), X)) → PR_IN(X, s(Y))

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
U51(x1, x2, x3)  =  U51(x1, x2, x3)
U71(x1, x2, x3)  =  U71(x1, x2, x3)
TIMES_IN(x1, x2, x3)  =  TIMES_IN(x1, x2)
U41(x1, x2)  =  U41(x2)
DIV_IN(x1, x2, x3)  =  DIV_IN(x1, x2)
PRIME_IN(x1)  =  PRIME_IN(x1)
U81(x1, x2, x3)  =  U81(x2, x3)
U121(x1, x2, x3, x4)  =  U121(x4)
NEQ_IN(x1, x2)  =  NEQ_IN(x1, x2)
U91(x1, x2, x3)  =  U91(x3)
QUOT_IN(x1, x2, x3, x4)  =  QUOT_IN(x1, x2, x3)
U61(x1, x2, x3)  =  U61(x3)
PR_IN(x1, x2)  =  PR_IN(x1, x2)
U31(x1, x2, x3, x4)  =  U31(x4)
U101(x1, x2, x3)  =  U101(x3)
U131(x1, x2, x3, x4)  =  U131(x4)
U21(x1, x2, x3, x4, x5)  =  U21(x5)
NOT_DIVIDES_IN(x1, x2)  =  NOT_DIVIDES_IN(x1, x2)
U111(x1, x2, x3, x4)  =  U111(x2, x4)
U11(x1, x2, x3, x4)  =  U11(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

PRIME_IN(s(s(X))) → U41(X, pr_in(s(s(X)), s(X)))
PRIME_IN(s(s(X))) → PR_IN(s(s(X)), s(X))
PR_IN(X, s(s(Y))) → U51(X, Y, not_divides_in(s(s(Y)), X))
PR_IN(X, s(s(Y))) → NOT_DIVIDES_IN(s(s(Y)), X)
NOT_DIVIDES_IN(Y, X) → U71(Y, X, div_in(X, Y, U))
NOT_DIVIDES_IN(Y, X) → DIV_IN(X, Y, U)
DIV_IN(X, Y, Z) → U11(X, Y, Z, quot_in(X, Y, Y, Z))
DIV_IN(X, Y, Z) → QUOT_IN(X, Y, Y, Z)
QUOT_IN(X, 0, s(Z), s(U)) → U31(X, Z, U, quot_in(X, s(Z), s(Z), U))
QUOT_IN(X, 0, s(Z), s(U)) → QUOT_IN(X, s(Z), s(Z), U)
QUOT_IN(s(X), s(Y), Z, U) → U21(X, Y, Z, U, quot_in(X, Y, Z, U))
QUOT_IN(s(X), s(Y), Z, U) → QUOT_IN(X, Y, Z, U)
U71(Y, X, div_out(X, Y, U)) → U81(Y, X, times_in(U, Y, Z))
U71(Y, X, div_out(X, Y, U)) → TIMES_IN(U, Y, Z)
TIMES_IN(s(X), Y, Z) → U111(X, Y, Z, times_in(X, Y, U))
TIMES_IN(s(X), Y, Z) → TIMES_IN(X, Y, U)
U111(X, Y, Z, times_out(X, Y, U)) → U121(X, Y, Z, add_in(U, Y, Z))
U111(X, Y, Z, times_out(X, Y, U)) → ADD_IN(U, Y, Z)
ADD_IN(s(X), Y, s(Z)) → U131(X, Y, Z, add_in(X, Y, Z))
ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)
U81(Y, X, times_out(U, Y, Z)) → U91(Y, X, neq_in(X, Z))
U81(Y, X, times_out(U, Y, Z)) → NEQ_IN(X, Z)
NEQ_IN(s(X), s(Y)) → U101(X, Y, neq_in(X, Y))
NEQ_IN(s(X), s(Y)) → NEQ_IN(X, Y)
U51(X, Y, not_divides_out(s(s(Y)), X)) → U61(X, Y, pr_in(X, s(Y)))
U51(X, Y, not_divides_out(s(s(Y)), X)) → PR_IN(X, s(Y))

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)
U51(x1, x2, x3)  =  U51(x1, x2, x3)
U71(x1, x2, x3)  =  U71(x1, x2, x3)
TIMES_IN(x1, x2, x3)  =  TIMES_IN(x1, x2)
U41(x1, x2)  =  U41(x2)
DIV_IN(x1, x2, x3)  =  DIV_IN(x1, x2)
PRIME_IN(x1)  =  PRIME_IN(x1)
U81(x1, x2, x3)  =  U81(x2, x3)
U121(x1, x2, x3, x4)  =  U121(x4)
NEQ_IN(x1, x2)  =  NEQ_IN(x1, x2)
U91(x1, x2, x3)  =  U91(x3)
QUOT_IN(x1, x2, x3, x4)  =  QUOT_IN(x1, x2, x3)
U61(x1, x2, x3)  =  U61(x3)
PR_IN(x1, x2)  =  PR_IN(x1, x2)
U31(x1, x2, x3, x4)  =  U31(x4)
U101(x1, x2, x3)  =  U101(x3)
U131(x1, x2, x3, x4)  =  U131(x4)
U21(x1, x2, x3, x4, x5)  =  U21(x5)
NOT_DIVIDES_IN(x1, x2)  =  NOT_DIVIDES_IN(x1, x2)
U111(x1, x2, x3, x4)  =  U111(x2, x4)
U11(x1, x2, x3, x4)  =  U11(x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 5 SCCs with 19 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NEQ_IN(s(X), s(Y)) → NEQ_IN(X, Y)

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
NEQ_IN(x1, x2)  =  NEQ_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

NEQ_IN(s(X), s(Y)) → NEQ_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

NEQ_IN(s(X), s(Y)) → NEQ_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y, s(Z)) → ADD_IN(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
ADD_IN(x1, x2, x3)  =  ADD_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

ADD_IN(s(X), Y) → ADD_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TIMES_IN(s(X), Y, Z) → TIMES_IN(X, Y, U)

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
TIMES_IN(x1, x2, x3)  =  TIMES_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

TIMES_IN(s(X), Y, Z) → TIMES_IN(X, Y, U)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
TIMES_IN(x1, x2, x3)  =  TIMES_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

TIMES_IN(s(X), Y) → TIMES_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

QUOT_IN(s(X), s(Y), Z, U) → QUOT_IN(X, Y, Z, U)
QUOT_IN(X, 0, s(Z), s(U)) → QUOT_IN(X, s(Z), s(Z), U)

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
QUOT_IN(x1, x2, x3, x4)  =  QUOT_IN(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

QUOT_IN(s(X), s(Y), Z, U) → QUOT_IN(X, Y, Z, U)
QUOT_IN(X, 0, s(Z), s(U)) → QUOT_IN(X, s(Z), s(Z), U)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
QUOT_IN(x1, x2, x3, x4)  =  QUOT_IN(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

QUOT_IN(X, 0, s(Z)) → QUOT_IN(X, s(Z), s(Z))
QUOT_IN(s(X), s(Y), Z) → QUOT_IN(X, Y, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U51(X, Y, not_divides_out(s(s(Y)), X)) → PR_IN(X, s(Y))
PR_IN(X, s(s(Y))) → U51(X, Y, not_divides_in(s(s(Y)), X))

The TRS R consists of the following rules:

prime_in(s(s(X))) → U4(X, pr_in(s(s(X)), s(X)))
pr_in(X, s(s(Y))) → U5(X, Y, not_divides_in(s(s(Y)), X))
not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
U5(X, Y, not_divides_out(s(s(Y)), X)) → U6(X, Y, pr_in(X, s(Y)))
pr_in(X, s(0)) → pr_out(X, s(0))
U6(X, Y, pr_out(X, s(Y))) → pr_out(X, s(s(Y)))
U4(X, pr_out(s(s(X)), s(X))) → prime_out(s(s(X)))

The argument filtering Pi contains the following mapping:
prime_in(x1)  =  prime_in(x1)
s(x1)  =  s(x1)
U4(x1, x2)  =  U4(x2)
pr_in(x1, x2)  =  pr_in(x1, x2)
U5(x1, x2, x3)  =  U5(x1, x2, x3)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U6(x1, x2, x3)  =  U6(x3)
pr_out(x1, x2)  =  pr_out
prime_out(x1)  =  prime_out
U51(x1, x2, x3)  =  U51(x1, x2, x3)
PR_IN(x1, x2)  =  PR_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U51(X, Y, not_divides_out(s(s(Y)), X)) → PR_IN(X, s(Y))
PR_IN(X, s(s(Y))) → U51(X, Y, not_divides_in(s(s(Y)), X))

The TRS R consists of the following rules:

not_divides_in(Y, X) → U7(Y, X, div_in(X, Y, U))
U7(Y, X, div_out(X, Y, U)) → U8(Y, X, times_in(U, Y, Z))
div_in(X, Y, Z) → U1(X, Y, Z, quot_in(X, Y, Y, Z))
U8(Y, X, times_out(U, Y, Z)) → U9(Y, X, neq_in(X, Z))
U1(X, Y, Z, quot_out(X, Y, Y, Z)) → div_out(X, Y, Z)
times_in(s(X), Y, Z) → U11(X, Y, Z, times_in(X, Y, U))
times_in(0, Y, 0) → times_out(0, Y, 0)
U9(Y, X, neq_out(X, Z)) → not_divides_out(Y, X)
quot_in(X, 0, s(Z), s(U)) → U3(X, Z, U, quot_in(X, s(Z), s(Z), U))
quot_in(s(X), s(Y), Z, U) → U2(X, Y, Z, U, quot_in(X, Y, Z, U))
quot_in(0, s(Y), s(Z), 0) → quot_out(0, s(Y), s(Z), 0)
U11(X, Y, Z, times_out(X, Y, U)) → U12(X, Y, Z, add_in(U, Y, Z))
neq_in(s(X), s(Y)) → U10(X, Y, neq_in(X, Y))
neq_in(0, s(X)) → neq_out(0, s(X))
neq_in(s(X), 0) → neq_out(s(X), 0)
U3(X, Z, U, quot_out(X, s(Z), s(Z), U)) → quot_out(X, 0, s(Z), s(U))
U2(X, Y, Z, U, quot_out(X, Y, Z, U)) → quot_out(s(X), s(Y), Z, U)
U12(X, Y, Z, add_out(U, Y, Z)) → times_out(s(X), Y, Z)
U10(X, Y, neq_out(X, Y)) → neq_out(s(X), s(Y))
add_in(s(X), Y, s(Z)) → U13(X, Y, Z, add_in(X, Y, Z))
add_in(0, X, X) → add_out(0, X, X)
add_in(X, 0, X) → add_out(X, 0, X)
U13(X, Y, Z, add_out(X, Y, Z)) → add_out(s(X), Y, s(Z))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
not_divides_in(x1, x2)  =  not_divides_in(x1, x2)
U7(x1, x2, x3)  =  U7(x1, x2, x3)
div_in(x1, x2, x3)  =  div_in(x1, x2)
U1(x1, x2, x3, x4)  =  U1(x4)
quot_in(x1, x2, x3, x4)  =  quot_in(x1, x2, x3)
0  =  0
U3(x1, x2, x3, x4)  =  U3(x4)
U2(x1, x2, x3, x4, x5)  =  U2(x5)
quot_out(x1, x2, x3, x4)  =  quot_out(x4)
div_out(x1, x2, x3)  =  div_out(x3)
U8(x1, x2, x3)  =  U8(x2, x3)
times_in(x1, x2, x3)  =  times_in(x1, x2)
U11(x1, x2, x3, x4)  =  U11(x2, x4)
times_out(x1, x2, x3)  =  times_out(x3)
U12(x1, x2, x3, x4)  =  U12(x4)
add_in(x1, x2, x3)  =  add_in(x1, x2)
U13(x1, x2, x3, x4)  =  U13(x4)
add_out(x1, x2, x3)  =  add_out(x3)
U9(x1, x2, x3)  =  U9(x3)
neq_in(x1, x2)  =  neq_in(x1, x2)
U10(x1, x2, x3)  =  U10(x3)
neq_out(x1, x2)  =  neq_out
not_divides_out(x1, x2)  =  not_divides_out
U51(x1, x2, x3)  =  U51(x1, x2, x3)
PR_IN(x1, x2)  =  PR_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U51(X, Y, not_divides_out) → PR_IN(X, s(Y))
PR_IN(X, s(s(Y))) → U51(X, Y, not_divides_in(s(s(Y)), X))

The TRS R consists of the following rules:

not_divides_in(Y, X) → U7(Y, X, div_in(X, Y))
U7(Y, X, div_out(U)) → U8(X, times_in(U, Y))
div_in(X, Y) → U1(quot_in(X, Y, Y))
U8(X, times_out(Z)) → U9(neq_in(X, Z))
U1(quot_out(Z)) → div_out(Z)
times_in(s(X), Y) → U11(Y, times_in(X, Y))
times_in(0, Y) → times_out(0)
U9(neq_out) → not_divides_out
quot_in(X, 0, s(Z)) → U3(quot_in(X, s(Z), s(Z)))
quot_in(s(X), s(Y), Z) → U2(quot_in(X, Y, Z))
quot_in(0, s(Y), s(Z)) → quot_out(0)
U11(Y, times_out(U)) → U12(add_in(U, Y))
neq_in(s(X), s(Y)) → U10(neq_in(X, Y))
neq_in(0, s(X)) → neq_out
neq_in(s(X), 0) → neq_out
U3(quot_out(U)) → quot_out(s(U))
U2(quot_out(U)) → quot_out(U)
U12(add_out(Z)) → times_out(Z)
U10(neq_out) → neq_out
add_in(s(X), Y) → U13(add_in(X, Y))
add_in(0, X) → add_out(X)
add_in(X, 0) → add_out(X)
U13(add_out(Z)) → add_out(s(Z))

The set Q consists of the following terms:

not_divides_in(x0, x1)
U7(x0, x1, x2)
div_in(x0, x1)
U8(x0, x1)
U1(x0)
times_in(x0, x1)
U9(x0)
quot_in(x0, x1, x2)
U11(x0, x1)
neq_in(x0, x1)
U3(x0)
U2(x0)
U12(x0)
U10(x0)
add_in(x0, x1)
U13(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


PR_IN(X, s(s(Y))) → U51(X, Y, not_divides_in(s(s(Y)), X))
The remaining pairs can at least be oriented weakly.

U51(X, Y, not_divides_out) → PR_IN(X, s(Y))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(PR_IN(x1, x2)) = x2   
POL(U1(x1)) = 0   
POL(U10(x1)) = 0   
POL(U11(x1, x2)) = 0   
POL(U12(x1)) = 0   
POL(U13(x1)) = 1 + x1   
POL(U2(x1)) = 0   
POL(U3(x1)) = 0   
POL(U51(x1, x2, x3)) = 1 + x2   
POL(U7(x1, x2, x3)) = 0   
POL(U8(x1, x2)) = 0   
POL(U9(x1)) = 0   
POL(add_in(x1, x2)) = 1 + x1 + x2   
POL(add_out(x1)) = 1   
POL(div_in(x1, x2)) = 0   
POL(div_out(x1)) = 0   
POL(neq_in(x1, x2)) = 0   
POL(neq_out) = 0   
POL(not_divides_in(x1, x2)) = 0   
POL(not_divides_out) = 0   
POL(quot_in(x1, x2, x3)) = 0   
POL(quot_out(x1)) = 0   
POL(s(x1)) = 1 + x1   
POL(times_in(x1, x2)) = 0   
POL(times_out(x1)) = 0   

The following usable rules [17] were oriented: none



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U51(X, Y, not_divides_out) → PR_IN(X, s(Y))

The TRS R consists of the following rules:

not_divides_in(Y, X) → U7(Y, X, div_in(X, Y))
U7(Y, X, div_out(U)) → U8(X, times_in(U, Y))
div_in(X, Y) → U1(quot_in(X, Y, Y))
U8(X, times_out(Z)) → U9(neq_in(X, Z))
U1(quot_out(Z)) → div_out(Z)
times_in(s(X), Y) → U11(Y, times_in(X, Y))
times_in(0, Y) → times_out(0)
U9(neq_out) → not_divides_out
quot_in(X, 0, s(Z)) → U3(quot_in(X, s(Z), s(Z)))
quot_in(s(X), s(Y), Z) → U2(quot_in(X, Y, Z))
quot_in(0, s(Y), s(Z)) → quot_out(0)
U11(Y, times_out(U)) → U12(add_in(U, Y))
neq_in(s(X), s(Y)) → U10(neq_in(X, Y))
neq_in(0, s(X)) → neq_out
neq_in(s(X), 0) → neq_out
U3(quot_out(U)) → quot_out(s(U))
U2(quot_out(U)) → quot_out(U)
U12(add_out(Z)) → times_out(Z)
U10(neq_out) → neq_out
add_in(s(X), Y) → U13(add_in(X, Y))
add_in(0, X) → add_out(X)
add_in(X, 0) → add_out(X)
U13(add_out(Z)) → add_out(s(Z))

The set Q consists of the following terms:

not_divides_in(x0, x1)
U7(x0, x1, x2)
div_in(x0, x1)
U8(x0, x1)
U1(x0)
times_in(x0, x1)
U9(x0)
quot_in(x0, x1, x2)
U11(x0, x1)
neq_in(x0, x1)
U3(x0)
U2(x0)
U12(x0)
U10(x0)
add_in(x0, x1)
U13(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.